\begin{tabbing}
(\=$\backslash$p. \+
\\[0ex]let i = get\_int\_arg `i` p 
\\[0ex]in let x = get\_term\_arg `x` p 
\\[0ex]
\\[0ex]in let e = get\_term\_arg `e` p 
\\[0ex]in let A = get\_term\_arg `A` p 
\\[0ex]in\= \+
\\[0ex]A\=ssertAtHyp \+
\\[0ex]i
\\[0ex]
\\[0ex](mk\_exists\_term (dv x) A (mk\_equal\_term A e x)) 
\\[0ex]p)
\-\-\-
\end{tabbing}